<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"/><meta name="viewport" content="width=device-width, initial-scale=0.8"/><title>Index</title><link rel="stylesheet" type="text/css" href="../scribble.css" title="default"/><link rel="stylesheet" type="text/css" href="../racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-style.css" title="default"/><link rel="stylesheet" type="text/css" href="../manual-racket.css" title="default"/><link rel="stylesheet" type="text/css" href="../doc-site.css" title="default"/><script type="text/javascript" src="../scribble-common.js"></script><script type="text/javascript" src="../manual-racket.js"></script><script type="text/javascript" src="../doc-site.js"></script><script type="text/javascript" src="../local-redirect/local-redirect.js"></script><script type="text/javascript" src="../local-redirect/local-user-redirect.js"></script><!--[if IE 6]><style type="text/css">.SIEHidden { overflow: hidden; }</style><![endif]--></head><body id="doc-racket-lang-org"><div class="tocset"><div class="tocview"><div class="tocviewlist tocviewlisttopspace"><div class="tocviewtitle"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,&quot;tocview_0&quot;);">&#9660;</a></td><td></td><td><a href="index.html" class="tocviewlink" data-pltdoc="x">Redex:<span class="mywbr"> &nbsp;</span> Practical Semantics Engineering</a></td></tr></table></div><div class="tocviewsublistonly" style="display: block;" id="tocview_0"><table cellspacing="0" cellpadding="0"><tr><td align="right">1&nbsp;</td><td><a href="tutorial.html" class="tocviewlink" data-pltdoc="x">Amb:<span class="mywbr"> &nbsp;</span> A Redex Tutorial</a></td></tr><tr><td align="right">2&nbsp;</td><td><a href="redex2015.html" class="tocviewlink" data-pltdoc="x">Long Tutorial</a></td></tr><tr><td align="right">3&nbsp;</td><td><a href="fri-mor.html" class="tocviewlink" data-pltdoc="x">Extended Exercises</a></td></tr><tr><td align="right">4&nbsp;</td><td><a href="The_Redex_Reference.html" class="tocviewlink" data-pltdoc="x">The Redex Reference</a></td></tr><tr><td align="right">5&nbsp;</td><td><a href="benchmark.html" class="tocviewlink" data-pltdoc="x">Automated Testing Benchmark</a></td></tr><tr><td align="right"></td><td><a href="doc-bibliography.html" class="tocviewlink" data-pltdoc="x">Bibliography</a></td></tr><tr><td align="right"></td><td><a href="" class="tocviewselflink" data-pltdoc="x">Index</a></td></tr></table></div></div></div></div><div class="maincolumn"><div class="main"><div class="navsettop"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" tabindex="1" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, &quot;7.7&quot;, &quot;../&quot;);" onfocus="this.style.color=&quot;black&quot;; this.style.textAlign=&quot;left&quot;; if (this.value == &quot;...search manuals...&quot;) this.value=&quot;&quot;;" onblur="if (this.value.match(/^ *$/)) { this.style.color=&quot;#888&quot;; this.style.textAlign=&quot;center&quot;; this.value=&quot;...search manuals...&quot;; }"/></form>&nbsp;&nbsp;<a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot(&quot;7.7&quot;);">top</a></span><span class="navright">&nbsp;&nbsp;<a href="doc-bibliography.html" title="backward to &quot;Bibliography&quot;" data-pltdoc="x">&larr; prev</a>&nbsp;&nbsp;<a href="index.html" title="up to &quot;Redex: Practical Semantics Engineering&quot;" data-pltdoc="x">up</a>&nbsp;&nbsp;<span class="nonavigation">next &rarr;</span></span>&nbsp;</div><h3 x-source-module="(lib &quot;redex/redex.scrbl&quot;)" x-source-pkg="redex-doc" x-part-tag="&quot;doc-index&quot;"><a name="(part._doc-index)"></a>Index</h3><table cellspacing="0" cellpadding="0"><tr><td><p><a href="#alpha:A">A</a> <a href="#alpha:B">B</a> <a href="#alpha:C">C</a> <a href="#alpha:D">D</a> <a href="#alpha:E">E</a> <a href="#alpha:F">F</a> <a href="#alpha:G">G</a> <a href="#alpha:H">H</a> <a href="#alpha:I">I</a> <a href="#alpha:J">J</a> <span class="nonavigation">K</span> <a href="#alpha:L">L</a> <a href="#alpha:M">M</a> <a href="#alpha:N">N</a> <a href="#alpha:O">O</a> <a href="#alpha:P">P</a> <span class="nonavigation">Q</span> <a href="#alpha:R">R</a> <a href="#alpha:S">S</a> <a href="#alpha:T">T</a> <a href="#alpha:U">U</a> <a href="#alpha:V">V</a> <a href="#alpha:W">W</a> <span class="nonavigation">X</span> <span class="nonavigation">Y</span> <span class="nonavigation">Z</span> </p></td></tr><tr><td><p>&nbsp;</p></td></tr><tr><td><p><a href="redex2015.html#%28part._close..rkt%29" class="indexlink" data-pltdoc="x"><span class="stt">"close.rkt"</span><br/></a><a href="redex2015.html#%28part._common..rkt%29" class="indexlink" data-pltdoc="x"><span class="stt">"common.rkt"</span><br/></a><a href="redex2015.html#%28part._extend-lookup..rkt%29" class="indexlink" data-pltdoc="x"><span class="stt">"extend-lookup.rkt"</span><br/></a><a href="redex2015.html#%28part._tc-common..rkt%29" class="indexlink" data-pltdoc="x"><span class="stt">"tc-common.rkt"</span><br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._24._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktPn">#:...bind</span><br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._23._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktPn">#:exports</span><br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._22._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktPn">#:refers-to</span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._--~3e%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink"><span class="nobreak">--&gt;</span></span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._~3a~3a~3d%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">::=</span></span><br/></a><a href="The_Redex_Reference.html#%28tech.__%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">_</span></span></span><br/></a><a name="alpha:A"></a><span><a href="redex2015.html#%28part._wed-aft%29" class="indexlink" data-pltdoc="x">Abstract Machines<br/></a></span><a href="redex2015.html#%28part._thu-mor%29" class="indexlink" data-pltdoc="x">Abstracting Abstract Machines<br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark%2Fmodels%2Fall-info..rkt%29._all-mods%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym">all-mods</span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._alpha-equivalent~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">alpha-equivalent?</span></span><br/></a><a href="tutorial.html" class="indexlink" data-pltdoc="x">Amb: A Redex Tutorial<br/></a><a href="The_Redex_Reference.html#%28tech._any%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">any</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._apply-reduction-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">apply-reduction-relation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._apply-reduction-relation%2A%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">apply-reduction-relation*</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._apply-reduction-relation%2Ftag-with-names%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">apply-reduction-relation/tag-with-names</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._arrow-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">arrow-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._arrow-space%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">arrow-space</span></span><br/></a><a href="benchmark.html" class="indexlink" data-pltdoc="x">Automated Testing Benchmark<br/></a><a name="alpha:B"></a><span><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._benchmark-logging-to%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">benchmark-logging-to</span></span><br/></a></span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._bind%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bind</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._bind-exp%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bind-exp</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._bind-name%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bind-name</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._bind~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bind?</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Binding_.Forms%29" class="indexlink" data-pltdoc="x">Binding Forms<br/></a><a href="The_Redex_Reference.html#%28tech._binding._form%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">binding forms</span><br/></a><a href="The_Redex_Reference.html#%28part._.Binding_.Repetitions%29" class="indexlink" data-pltdoc="x">Binding Repetitions<br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-data%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bmark-log-data</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-data-data%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bmark-log-data-data</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-data~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bmark-log-data?</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._bmark-log-directory%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">bmark-log-directory</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._boolean%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">boolean</span></span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._build-derivations%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">build-derivations</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._build-lw%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">build-lw</span></span><br/></a><a name="alpha:C"></a><span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._caching-enabled~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">caching-enabled?</span></span><br/></a></span><a href="redex2015.html#%28tech._calculu%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">calculus</span><br/></a><a href="redex2015.html#%28part._.C.C_.Machine%29" class="indexlink" data-pltdoc="x">CC Machine<br/></a><a href="benchmark.html#%28tech._check%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">check</span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._check-metafunction%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">check-metafunction</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._check-reduction-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">check-reduction-relation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._check-redundancy%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">check-redundancy</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._compatible-closure%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">compatible-closure</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._compatible._closure._context%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">compatible-closure-context</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._compiled-lang~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">compiled-lang?</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Compound_.Forms_with_.Binders%29" class="indexlink" data-pltdoc="x">Compound Forms with Binders<br/></a><a href="redex2015.html#%28tech._computation%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">computations</span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._context-closure%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">context-closure</span></span><br/></a><a href="redex2015.html#%28part._.Contexts__.Values%29" class="indexlink" data-pltdoc="x">Contexts, Values<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._counterexample%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">counterexample</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._counterexample-term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">counterexample-term</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._counterexample~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">counterexample?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._coverage~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">coverage?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._covered-cases%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">covered-cases</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._cros%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">cross</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._curly-quotes-for-strings%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">curly-quotes-for-strings</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._current-cache-all~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">current-cache-all?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._current-render-pict-adjust%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">current-render-pict-adjust</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._current-text%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">current-text</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._current-traced-metafunctions%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">current-traced-metafunctions</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Customization%29" class="indexlink" data-pltdoc="x">Customization<br/></a><a name="alpha:D"></a><span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._dark-brush-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">dark-brush-color</span></span><br/></a></span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._dark-pen-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">dark-pen-color</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._dark-text-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">dark-text-color</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._debugging._plt._redex._program%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">Debugging PLT Redex Programs</span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._default-attempt-size%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-attempt-size</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._default-check-attempts%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-check-attempts</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._default-equiv%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-equiv</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._default-font-size%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-font-size</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._default-language%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-language</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._default-pretty-printer%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-pretty-printer</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._default-relation-clause-combine%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-relation-clause-combine</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._default-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-style</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._default-white-square-bracket%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">default-white-square-bracket</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-extended-judgment-form%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-extended-judgment-form</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-extended-language%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-extended-language</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-judgment-form%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-judgment-form</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-language%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-language</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-metafunction%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-metafunction</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-metafunction%2Fextension%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-metafunction/extension</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-relation</span></span><br/></a><a href="benchmark.html#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-rewrite</span></span><br/></a><a href="benchmark.html#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._define-rewrite%2Fcompose%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-rewrite/compose</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-term</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._define-union-language%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">define-union-language</span></span><br/></a><a href="tutorial.html#%28part._.Defining_a_.Language%29" class="indexlink" data-pltdoc="x">Defining a Language<br/></a><a href="tutorial.html#%28part._.Defining_a_.Reduction_.Relation%29" class="indexlink" data-pltdoc="x">Defining a Reduction Relation<br/></a><a href="benchmark.html#%28part._sec~3ab~3adelim-cont%29" class="indexlink" data-pltdoc="x">delim-cont<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._delimit-ellipsis-arguments~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">delimit-ellipsis-arguments?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._depth-dependent-order~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">depth-dependent-order?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._derivation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._derivation-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._derivation-name%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation-name</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._derivation-subs%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation-subs</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._derivation-term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation-term</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._derivation%2Fps%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation/ps</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._derivation~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">derivation?</span></span><br/></a><a href="redex2015.html#%28part._.Developing_a_.Language%29" class="indexlink" data-pltdoc="x">Developing a Language<br/></a><a href="redex2015.html#%28part._.Developing_a_.Language_2%29" class="indexlink" data-pltdoc="x">Developing a Language 2<br/></a><a href="redex2015.html#%28part._.Developing_.Metafunctions%29" class="indexlink" data-pltdoc="x">Developing Metafunctions<br/></a><a href="redex2015.html#%28part._.Developing_.Type_.Judgments%29" class="indexlink" data-pltdoc="x">Developing Type Judgments<br/></a><a name="alpha:E"></a><span><a href="The_Redex_Reference.html#%28part._.Ellipses_in_.Binding_.Forms%29" class="indexlink" data-pltdoc="x">Ellipses in Binding Forms<br/></a></span><a href="redex2015.html#%28tech._environment%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">environment</span><br/></a><a href="redex2015.html#%28part._lma%29" class="indexlink" data-pltdoc="x">Exercises<br/></a><a href="redex2015.html#%28part._lta%29" class="indexlink" data-pltdoc="x">Exercises<br/></a><a href="redex2015.html#%28part._ltm%29" class="indexlink" data-pltdoc="x">Exercises<br/></a><a href="redex2015.html#%28part._lwa%29" class="indexlink" data-pltdoc="x">Exercises<br/></a><a href="redex2015.html#%28part._lwm%29" class="indexlink" data-pltdoc="x">Exercises<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._exn~3afail~3aredex~3ageneration-failure~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">exn:fail:redex:generation-failure?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._exn~3afail~3aredex~3atest%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">exn:fail:redex:test</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._exn~3afail~3aredex~3atest-source%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">exn:fail:redex:test-source</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._exn~3afail~3aredex~3atest-term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">exn:fail:redex:test-term</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._exn~3afail~3aredex~3atest~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">exn:fail:redex:test?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._exn~3afail~3aredex~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">exn:fail:redex?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._extend-language-show-extended-order%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">extend-language-show-extended-order</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._extend-language-show-union%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">extend-language-show-union</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._extend-reduction-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">extend-reduction-relation</span></span><br/></a><a href="fri-mor.html" class="indexlink" data-pltdoc="x">Extended Exercises<br/></a><a href="redex2015.html#%28part._.Extending_a_.Language__any%29" class="indexlink" data-pltdoc="x">Extending a Language: <span class="RktSym">any</span><br/></a><a name="alpha:F"></a><span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._fill-between%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">fill-between</span></span><br/></a></span><a href="benchmark.html#%28part._sec~3afinding%29" class="indexlink" data-pltdoc="x">Finding the Benchmark Models<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._fresh%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">fresh</span></span><br/></a><a name="alpha:G"></a><span><a href="benchmark.html#%28tech._generate%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">generate</span><br/></a></span><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._generate-term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">generate-term</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._grammar-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">grammar-style</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.G.U.I%29" class="indexlink" data-pltdoc="x">GUI<br/></a><a name="alpha:H"></a><span><a href="The_Redex_Reference.html#%28tech._hide._hole%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">hide-hole</span></span></span><br/></a></span><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._hole%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">hole</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._hole%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">hole</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._homemade-white-square-bracket%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">homemade-white-square-bracket</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._horizontal-bar-spacing%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">horizontal-bar-spacing</span></span><br/></a><a name="alpha:I"></a><span><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._.I%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">I</span></span><br/></a></span><a href="redex2015.html#%28part._wed-mor%29" class="indexlink" data-pltdoc="x">Imperative Extensions<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._in-domain~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">in-domain?</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._in-hole%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">in-hole</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._in._hole%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">in-hole</span></span></span><br/></a><a href="benchmark.html#%28form._%28%28lib._redex%2Fbenchmark..rkt%29._include%2Frewrite%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">include/rewrite</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._initial-char-width%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">initial-char-width</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._initial-font-size%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">initial-font-size</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._integer%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">integer</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._.I.O-judgment-form~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">IO-judgment-form?</span></span><br/></a><a name="alpha:J"></a><span><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._judgment-form-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">judgment-form-&gt;pict</span></span><br/></a></span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._judgment-form-cases%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">judgment-form-cases</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._judgment-form-show-rule-names%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">judgment-form-show-rule-names</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._judgment-form~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">judgment-form?</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._judgment-holds%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">judgment-holds</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._just-after%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">just-after</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._just-before%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">just-before</span></span><br/></a><a name="alpha:L"></a><span><a href="redex2015.html#%28part._lab-wed-mor%29" class="indexlink" data-pltdoc="x"><span style="font-weight: bold">Lab</span> Contexts and Stores<br/></a></span><a href="redex2015.html#%28part._lab-mon-aft%29" class="indexlink" data-pltdoc="x"><span style="font-weight: bold">Lab</span> Designing Metafunctions<br/></a><a href="redex2015.html#%28part._lab-tue-mor%29" class="indexlink" data-pltdoc="x"><span style="font-weight: bold">Lab</span> Designing Reductions<br/></a><a href="redex2015.html#%28part._lab-wed-aft%29" class="indexlink" data-pltdoc="x"><span style="font-weight: bold">Lab</span> Machine Transitions<br/></a><a href="redex2015.html#%28part._lab-tue-aft%29" class="indexlink" data-pltdoc="x"><span style="font-weight: bold">Lab</span> Type Checking<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._label-font-size%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">label-font-size</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._label-space%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">label-space</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._label-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">label-style</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._language-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">language-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._language-nts%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">language-nts</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Languages%29" class="indexlink" data-pltdoc="x">Languages<br/></a><a href="The_Redex_Reference.html#%28tech._lc._lang%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic"><span class="RktVar">lc-lang</span></span><br/></a><a href="benchmark.html#%28part._sec~3ab~3alet-poly%29" class="indexlink" data-pltdoc="x">let-poly<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._light-brush-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">light-brush-color</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._light-pen-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">light-pen-color</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._light-text-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">light-text-color</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._linebreaks%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">linebreaks</span></span><br/></a><a href="benchmark.html#%28part._sec~3ab~3alist-machine%29" class="indexlink" data-pltdoc="x">list-machine<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._literal-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">literal-style</span></span><br/></a><a href="benchmark.html#%28part._log%29" class="indexlink" data-pltdoc="x">Logging<br/></a><a href="redex2015.html" class="indexlink" data-pltdoc="x">Long Tutorial<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-column%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-column</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-column-span%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-column-span</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-e%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-e</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-line%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-line</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-line-span%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-line-span</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-metafunction~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-metafunction?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw-unq~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw-unq?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._lw~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">lw?</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.L.Ws%29" class="indexlink" data-pltdoc="x">LWs<br/></a><a name="alpha:M"></a><span><a href="The_Redex_Reference.html#%28part._.Macros_and_.Typesetting%29" class="indexlink" data-pltdoc="x">Macros and Typesetting<br/></a></span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._make-bind%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-bind</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._make-binding-hash%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-binding-hash</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._make-counterexample%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-counterexample</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._make-coverage%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">make-coverage</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._make-derivation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-derivation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._make-exn~3afail~3aredex~3atest%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-exn:fail:redex:test</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._make-immutable-binding-hash%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-immutable-binding-hash</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._make-lw%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">make-lw</span></span><br/></a><a href="benchmark.html#%28part._manage%29" class="indexlink" data-pltdoc="x">Managing Benchmark Modules<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._match-bindings%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">match-bindings</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._match~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">match?</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._metafunction%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">metafunction</span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._metafunction-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">metafunction-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-arrow-pict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-arrow-pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-cases%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-cases</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-combine-contract-and-rules%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-combine-contract-and-rules</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-fill-acceptable-width%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-fill-acceptable-width</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-font-size%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-font-size</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-gap-space%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-gap-space</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-line-gap-space%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-line-gap-space</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-pict-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-pict-style</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-rule-gap-space%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-rule-gap-space</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-style</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._metafunction-up%2Fdown-indent%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">metafunction-up/down-indent</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._metafunctions-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">metafunctions-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._mf-apply%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">mf-apply</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Multiple_.Variables_in_a_.Single_.Scope%29" class="indexlink" data-pltdoc="x">Multiple Variables in a Single Scope<br/></a><a name="alpha:N"></a><span><a href="The_Redex_Reference.html#%28tech._name%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">name</span></span></span><br/></a></span><a href="The_Redex_Reference.html#%28tech._natural%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">natural</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._non-terminal-gap-space%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">non-terminal-gap-space</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._non-terminal-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">non-terminal-style</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._non-terminal-subscript-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">non-terminal-subscript-style</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._non-terminal-superscript-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">non-terminal-superscript-style</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._nothing%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">nothing</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._number%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">number</span></span></span><br/></a><a name="alpha:O"></a><span><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._.O%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">O</span></span><br/></a></span><a href="The_Redex_Reference.html#%28part._.Other_.Relations%29" class="indexlink" data-pltdoc="x">Other Relations<br/></a><a href="The_Redex_Reference.html#%28tech._other._literal%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktVar">other-literal</span></span></span><br/></a><a name="alpha:P"></a><span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._paren-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">paren-style</span></span><br/></a></span><a href="The_Redex_Reference.html#%28tech._pattern%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">pattern</span><br/></a><a href="The_Redex_Reference.html#%28tech._pattern._sequence%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktVar">pattern-sequence</span></span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Patterns%29" class="indexlink" data-pltdoc="x">Patterns<br/></a><a href="The_Redex_Reference.html#%28part._.Picts__.P.D.F____.Post.Script%29" class="indexlink" data-pltdoc="x">Picts, PDF, &amp; PostScript<br/></a><a href="benchmark.html#%28part._.Plotting%29" class="indexlink" data-pltdoc="x">Plotting<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._plug%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">plug</span></span><br/></a><a href="benchmark.html#%28part._sec~3ab~3apoly-stlc%29" class="indexlink" data-pltdoc="x">poly-stlc<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._pretty-print-parameters%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">pretty-print-parameters</span></span><br/></a><a href="Problem__Binary_Addition.html" class="indexlink" data-pltdoc="x">Problem: Binary Addition<br/></a><a href="Problem__Contracts.html" class="indexlink" data-pltdoc="x">Problem: Contracts<br/></a><a href="Problem__Finite_State_Machines.html" class="indexlink" data-pltdoc="x">Problem: Finite State Machines<br/></a><a href="Problem__GC.html" class="indexlink" data-pltdoc="x">Problem: GC<br/></a><a href="Problem__Missionaries_and_Cannibals.html" class="indexlink" data-pltdoc="x">Problem: Missionaries and Cannibals<br/></a><a href="Problem__Objects.html" class="indexlink" data-pltdoc="x">Problem: Objects<br/></a><a href="Problem__Threads.html" class="indexlink" data-pltdoc="x">Problem: Threads<br/></a><a href="Problem__Towers_of_Hanoi.html" class="indexlink" data-pltdoc="x">Problem: Towers of Hanoi<br/></a><a href="Problem__Types.html" class="indexlink" data-pltdoc="x">Problem: Types<br/></a><a href="redex2015.html#%28tech._program%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">Program</span><br/></a><a name="alpha:R"></a><span><a href="redex2015.html#%28part._.Raising_.Exceptions%29" class="indexlink" data-pltdoc="x">Raising Exceptions<br/></a></span><a href="tutorial.html#%28part._.Random_.Testing%29" class="indexlink" data-pltdoc="x">Random Testing<br/></a><a href="benchmark.html#%28part._sec~3ab~3arbtrees%29" class="indexlink" data-pltdoc="x">rbtrees<br/></a><a href="The_Redex_Reference.html#%28tech._real%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">real</span></span></span><br/></a><a href="The_Redex_Reference.html" class="indexlink" data-pltdoc="x"><span class="RktModLink"><span class="RktSym">redex</span></span><br/></a><a href="redex2015.html#%28tech._redex%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">redex</span><br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._10._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, variable-prefix<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._11._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, variable-not-otherwise-mentioned<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._9._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, variable-except<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._8._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, variable<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._13._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, symbol<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._6._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, string<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._17._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, side-condition<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._5._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, real<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._20._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, pattern-sequence<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._21._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, other-literal<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._2._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, number<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._3._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, natural<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._14._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, name<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._4._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, integer<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._15._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, in-hole<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._12._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, hole<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._16._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, hide-hole<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._19._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, cross<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._18._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, compatible-closure-context<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._7._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, boolean<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._0._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, any<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._1._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x">Redex Pattern, _<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-check%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-check</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-enum%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-enum</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-generator%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-generator</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-index%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-index</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-let%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-let</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-let%2A%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-let*</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-match%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-match</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-match~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">redex-match?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._redex-pseudo-random-generator%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">redex-pseudo-random-generator</span></span><br/></a><a href="benchmark.html" class="indexlink" data-pltdoc="x"><span class="RktModLink"><span class="RktSym">redex/benchmark</span></span><br/></a><a href="benchmark.html#%28mod-path._redex%2Fbenchmark%2Fmodels%2Fall-info%29" class="indexlink" data-pltdoc="x"><span class="RktModLink"><span class="RktSym">redex/benchmark/models/all-info</span></span><br/></a><a href="The_Redex_Reference.html#%28mod-path._redex%2Fgui%29" class="indexlink" data-pltdoc="x"><span class="RktModLink"><span class="RktSym">redex/gui</span></span><br/></a><a href="The_Redex_Reference.html#%28mod-path._redex%2Fpict%29" class="indexlink" data-pltdoc="x"><span class="RktModLink"><span class="RktSym">redex/pict</span></span><br/></a><a href="The_Redex_Reference.html#%28mod-path._redex%2Freduction-semantics%29" class="indexlink" data-pltdoc="x"><span class="RktModLink"><span class="RktSym">redex/reduction-semantics</span></span><br/></a><a href="index.html" class="indexlink" data-pltdoc="x">Redex: Practical Semantics Engineering<br/></a><a href="redex2015.html#%28part._.Long_.Tutorial_.Reduction_.Relations%29" class="indexlink" data-pltdoc="x">Reduction Relations<br/></a><a href="The_Redex_Reference.html#%28part._.Reduction_.Relations%29" class="indexlink" data-pltdoc="x">Reduction Relations<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._reduction-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">reduction-relation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._reduction-relation-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-relation-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._reduction-relation-~3erule-names%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-relation-&gt;rule-names</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._reduction-relation-rule-extra-separation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-relation-rule-extra-separation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._reduction-relation-rule-line-separation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-relation-rule-line-separation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._reduction-relation-rule-separation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-relation-rule-separation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._reduction-relation~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-relation?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._reduction-rule-style%2Fc%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-rule-style/c</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._reduction-steps-cutoff%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">reduction-steps-cutoff</span></span><br/></a><a href="redex2015.html#%28part._tue-mor%29" class="indexlink" data-pltdoc="x">Reductions and Semantics<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._relation-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">relation-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._relation-clause-combine%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">relation-clause-combine</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._relation-clauses-combine%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">relation-clauses-combine</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._relation-coverage%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">relation-coverage</span></span><br/></a><a href="The_Redex_Reference.html#%28part._pink%29" class="indexlink" data-pltdoc="x">Removing the Pink Background<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._render-judgment-form%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">render-judgment-form</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._render-language%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">render-language</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._render-language-nts%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">render-language-nts</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._render-lw%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">render-lw</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._render-metafunction%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">render-metafunction</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._render-metafunctions%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">render-metafunctions</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._render-reduction-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">render-reduction-relation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._render-reduction-relation-rules%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">render-reduction-relation-rules</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._render-relation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">render-relation</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._render-term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">render-term</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._render-term%2Fpretty-write%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">render-term/pretty-write</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info-~3eside-condition-pict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info-&gt;side-condition-pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info-arrow%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info-arrow</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info-computed-label%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info-computed-label</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info-label%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info-label</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info-lhs%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info-lhs</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info-rhs%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info-rhs</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-info~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-info?</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._rule-pict-style%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">rule-pict-style</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-gen-and-check</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-gen-and-check%2Fmods%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-gen-and-check/mods</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-results</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results-cexps%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-results-cexps</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results-time%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-results-time</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results-tries%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-results-tries</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._run-results~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">run-results?</span></span><br/></a><a href="benchmark.html#%28part._run%29" class="indexlink" data-pltdoc="x">Running Benchmark Models<br/></a><a href="benchmark.html#%28part._sec~3ab~3arvm%29" class="indexlink" data-pltdoc="x">rvm<br/></a><a name="alpha:S"></a><span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._sc-linebreaks%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">sc-linebreaks</span></span><br/></a></span><a href="redex2015.html#%28tech._scope%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">scope</span><br/></a><a href="redex2015.html#%28part._.Semantics%29" class="indexlink" data-pltdoc="x">Semantics<br/></a><a href="redex2015.html#%28tech._semantic%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">semantics</span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-arrow-pict%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-arrow-pict!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._set-cache-size%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-cache-size!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-column%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-column!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-column-span%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-column-span!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-e%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-e!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-line%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-line!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-line-span%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-line-span!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-metafunction~3f%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-metafunction?!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._set-lw-unq~3f%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">set-lw-unq?!</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._shadow%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">shadow</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._show-derivations%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">show-derivations</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._side._condition%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">side-condition</span></span></span><br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._25._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym">side-condition</span> clause<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._26._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym">side-condition/hidden</span> clause<br/></a><a href="Solution__Binary_Addition.html" class="indexlink" data-pltdoc="x">Solution: Binary Addition<br/></a><a href="Solution__Contracts.html" class="indexlink" data-pltdoc="x">Solution: Contracts<br/></a><a href="Solution__Finite_State_Machines.html" class="indexlink" data-pltdoc="x">Solution: Finite State Machines<br/></a><a href="Solution__GC.html" class="indexlink" data-pltdoc="x">Solution: GC<br/></a><a href="Solution__Missionaries_and_Cannibals.html" class="indexlink" data-pltdoc="x">Solution: Missionaries and Cannibals<br/></a><a href="Solution__Objects.html" class="indexlink" data-pltdoc="x">Solution: Objects<br/></a><a href="Solution__Threads.html" class="indexlink" data-pltdoc="x">Solution: Threads<br/></a><a href="Solution__Towers_of_Hanoi.html" class="indexlink" data-pltdoc="x">Solution: Towers of Hanoi<br/></a><a href="Solution__Types.html" class="indexlink" data-pltdoc="x">Solution: Types<br/></a><a href="redex2015.html#%28tech._standard._reduction%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">Standard reduction</span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._stepper%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">stepper</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._stepper%2Fseed%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">stepper/seed</span></span><br/></a><a href="benchmark.html#%28part._sec~3ab~3astlc%29" class="indexlink" data-pltdoc="x">stlc<br/></a><a href="benchmark.html#%28part._sec~3ab~3astlc-sub%29" class="indexlink" data-pltdoc="x">stlc-sub<br/></a><a href="The_Redex_Reference.html#%28tech._string%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">string</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._struct~3abind%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:bind</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._struct~3abmark-log-data%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:bmark-log-data</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._struct~3acounterexample%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:counterexample</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._struct~3aderivation%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:derivation</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._struct~3aexn~3afail~3aredex~3atest%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:exn:fail:redex:test</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._struct~3alw%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:lw</span></span><br/></a><a href="benchmark.html#%28def._%28%28lib._redex%2Fbenchmark..rkt%29._struct~3arun-results%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">struct:run-results</span></span><br/></a><a href="redex2015.html#%28part._.Subjection_.Reduction%29" class="indexlink" data-pltdoc="x">Subjection Reduction<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._substitute%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">substitute</span></span><br/></a><a href="redex2015.html#%28part._.Substitution%29" class="indexlink" data-pltdoc="x">Substitution<br/></a><a href="The_Redex_Reference.html#%28tech._symbol%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktVar">symbol</span></span></span><br/></a><a href="redex2015.html#%28part._mon-aft%29" class="indexlink" data-pltdoc="x">Syntax and Metafunctions<br/></a><a name="alpha:T"></a><span><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._term%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">term</span></span><br/></a></span><a href="The_Redex_Reference.html#%28tech._term%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">term</span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._term-~3epict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">term-&gt;pict</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._term-~3epict%2Fpretty-write%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-&gt;pict/pretty-write</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._term-let%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">term-let</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._term-match%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">term-match</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._term-match%2Fsingle%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">term-match/single</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-children%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-children</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-color%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-color</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-expr%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-expr</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-height%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-height</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-labels%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-labels</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-parents%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-parents</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-set-color%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-set-color!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-set-position%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-set-position!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-set-red%21%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-set-red!</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-width%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-width</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-x%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-x</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node-y%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node-y</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._term-node~3f%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">term-node?</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Terms%29" class="indexlink" data-pltdoc="x">Terms<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test--~3e%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test--&gt;</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test--~3e~3e%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test--&gt;&gt;</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test--~3e~3e.E%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test--&gt;&gt;E</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test--~3e~3e~e2~88~83%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test--&gt;&gt;&#8707;</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test-equal%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test-equal</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test-judgment-holds%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test-judgment-holds</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test-match%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test-match</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test-no-match%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test-no-match</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._test-predicate%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">test-predicate</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._test-results%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">test-results</span></span><br/></a><a href="The_Redex_Reference.html#%28part._.Testing%29" class="indexlink" data-pltdoc="x">Testing<br/></a><a href="tutorial.html#%28part._.Testing_.Reduction_.Relations%29" class="indexlink" data-pltdoc="x">Testing Reduction Relations<br/></a><a href="tutorial.html#%28part._.Testing_.Typing%29" class="indexlink" data-pltdoc="x">Testing Typing<br/></a><a href="benchmark.html#%28part._sec~3abenchmark%29" class="indexlink" data-pltdoc="x">The Benchmark Models<br/></a><a href="redex2015.html#%28part._.The_.C.C-.C.K_.Theorem%29" class="indexlink" data-pltdoc="x">The CC-CK Theorem<br/></a><a href="redex2015.html#%28part._.The_.C.E.K_machine%29" class="indexlink" data-pltdoc="x">The CEK machine<br/></a><a href="redex2015.html#%28part._.The_.C.E.K-.C.K_.Theorem%29" class="indexlink" data-pltdoc="x">The CEK-CK Theorem<br/></a><a href="redex2015.html#%28part._.The_.C.K_.Machine%29" class="indexlink" data-pltdoc="x">The CK Machine<br/></a><a href="The_Redex_Reference.html" class="indexlink" data-pltdoc="x">The Redex Reference<br/></a><a href="redex2015.html#%28part._mon-mor%29" class="indexlink" data-pltdoc="x">The Theoretical Framework<br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._to-lw%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">to-lw</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._to-lw%2Fstx%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">to-lw/stx</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._traces%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">traces</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fgui..rkt%29._traces%2Fps%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">traces/ps</span></span><br/></a><a href="redex2015.html#%28tech._truth%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">Truth</span><br/></a><a href="redex2015.html#%28part._.Types%29" class="indexlink" data-pltdoc="x">Types<br/></a><a href="redex2015.html#%28part._tue-aft%29" class="indexlink" data-pltdoc="x">Types and Property Testing<br/></a><a href="The_Redex_Reference.html#%28part._.Typesetting%29" class="indexlink" data-pltdoc="x">Typesetting<br/></a><a href="tutorial.html#%28part._.Typesetting_the_.Reduction_.Relation%29" class="indexlink" data-pltdoc="x">Typesetting the Reduction Relation<br/></a><a href="tutorial.html#%28part._.Typing%29" class="indexlink" data-pltdoc="x">Typing<br/></a><a name="alpha:U"></a><span><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._union-reduction-relations%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">union-reduction-relations</span></span><br/></a></span><a name="alpha:V"></a><span><a href="redex2015.html#%28tech._value%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic">Value</span><br/></a></span><a href="The_Redex_Reference.html#%28tech._variable%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">variable</span></span></span><br/></a><a href="redex2015.html#%28part._.Variable_.Assignment%29" class="indexlink" data-pltdoc="x">Variable Assignment<br/></a><a href="The_Redex_Reference.html#%28tech._variable._except%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">variable-except</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._variable-not-in%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">variable-not-in</span></span><br/></a><a href="The_Redex_Reference.html#%28tech._variable._not._otherwise._mentioned%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">variable-not-otherwise-mentioned</span></span></span><br/></a><a href="The_Redex_Reference.html#%28tech._variable._prefix%29" class="indexlink" data-pltdoc="x"><span class="techoutside"><span class="techinside"><span class="RktSym">variable-prefix</span></span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Freduction-semantics..rkt%29._variables-not-in%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">variables-not-in</span></span><br/></a><a name="alpha:W"></a><span><a href="redex2015.html#%28part._.What_are_.Models%29" class="indexlink" data-pltdoc="x">What are Models<br/></a></span><a href="The_Redex_Reference.html#%28tech._where._clause%29" class="indexlink" data-pltdoc="x"><span style="font-style: italic"><span class="RktSym">where</span> clause</span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._where-combine%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">where-combine</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._where-make-prefix-pict%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">where-make-prefix-pict</span></span><br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._28._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym">where/error</span> clause<br/></a><a href="The_Redex_Reference.html#%28idx._%28gentag._27._%28lib._redex%2Fredex..scrbl%29%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym">where/hidden</span> clause<br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._white-bracket-sizing%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">white-bracket-sizing</span></span><br/></a><a href="The_Redex_Reference.html#%28def._%28%28lib._redex%2Fpict..rkt%29._white-square-bracket%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktValLink">white-square-bracket</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Freduction-semantics..rkt%29._with%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">with</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-atomic-rewriter%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">with-atomic-rewriter</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-atomic-rewriters%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">with-atomic-rewriters</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-compound-rewriter%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">with-compound-rewriter</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-compound-rewriters%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">with-compound-rewriters</span></span><br/></a><a href="The_Redex_Reference.html#%28form._%28%28lib._redex%2Fpict..rkt%29._with-unquote-rewriter%29%29" class="indexlink" data-pltdoc="x"><span class="RktSym"><span class="RktStxLink">with-unquote-rewriter</span></span><br/></a></p></td></tr></table><div class="navsetbottom"><span class="navleft"><form class="searchform"><input class="searchbox" style="color: #888;" type="text" tabindex="1" value="...search manuals..." title="Enter a search string to search the manuals" onkeypress="return DoSearchKey(event, this, &quot;7.7&quot;, &quot;../&quot;);" onfocus="this.style.color=&quot;black&quot;; this.style.textAlign=&quot;left&quot;; if (this.value == &quot;...search manuals...&quot;) this.value=&quot;&quot;;" onblur="if (this.value.match(/^ *$/)) { this.style.color=&quot;#888&quot;; this.style.textAlign=&quot;center&quot;; this.value=&quot;...search manuals...&quot;; }"/></form>&nbsp;&nbsp;<a href="../index.html" title="up to the documentation top" data-pltdoc="x" onclick="return GotoPLTRoot(&quot;7.7&quot;);">top</a></span><span class="navright">&nbsp;&nbsp;<a href="doc-bibliography.html" title="backward to &quot;Bibliography&quot;" data-pltdoc="x">&larr; prev</a>&nbsp;&nbsp;<a href="index.html" title="up to &quot;Redex: Practical Semantics Engineering&quot;" data-pltdoc="x">up</a>&nbsp;&nbsp;<span class="nonavigation">next &rarr;</span></span>&nbsp;</div></div></div><div id="contextindicator">&nbsp;</div></body></html>